ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple{i:l}(ds; da),
L:(event-info(ds;da) List), m:.
ecl-trans-normal(v)
 (L1:(event-info(ds;da) List). 
 iseg(event-info(ds;da); L1; L)  (ecl-trans-halt2(ds; da; v)(0,L1))  False)
 ((ecl-trans-act(ds; da; v)(m,L))  (ecl-trans-act(ds; da; reset-ecl-tuple(v))(m,L))) 

latex

Definitions

x,y. t(x;y), list_accum(x,a.f(x;a); y; l), ecl-trans-init(v), ecl-trans-state-from(v; z; L), ecl-trans-h(v), ecl-trans-state(v; L), ecl-trans-halt2(ds; da; A), tt, t.1, ecl-trans-type(A), ff, if b then t else f fi , A c B, reset-ecl-tuple(A), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), event-info(ds;da), ecl-trans-tuple{i:l}(ds; da), Y, ||as||, subtype(S; T), top, x. t(x), A, A  B, prop{i:l}, t  T, P  Q, P  Q, P  Q, False, P  Q, , x:A. B(x), x(s1,s2), Unit, , spreadn(a; x,y,z.t(x;y;z)), x:A. B(x), ecl-trans-act(ds; da; A), P  Q, decidable(P), x(s), , ma-valtype(da; k)

Lemmas

ecl-trans-act-functionality2, not functionality wrt iff, assert-deq-member, deq-member wf, list accum append, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Kind-deq wf, fpf-cap wf, decl-state wf, eqtt to assert, subtype rel self, nat plus wf, bool wf, ma-valtype wf, l member wf, ecl-trans-state wf, append wf, ecl-trans-act functionality, length wf1, length append, iseg length, member wf, last wf, iseg append0, length wf nat, iseg transitivity, last lemma, decidable false, append is nil, assert of null, top wf, null wf3, decidable assert, Id wf, Knd wf, fpf wf, ecl-trans-tuple wf, nat wf, ecl-trans-normal wf, false wf, le wf, ecl-trans-halt2 wf, iseg wf, event-info wf, reset-ecl-tuple wf, ecl-trans-act wf